package stackcontract;

import com.google.java.contract.Ensures;
import com.google.java.contract.Invariant;
import com.google.java.contract.Requires;

@Invariant ("size()>=0")
public interface MyStack<T> {

	public int size();
	
	@Requires ("size()>=1")
	public T   peek();
	
	@Requires ("size()>=1")
	@Ensures ({"size()==old(size())-1"," result==old(peeck())"})
	public T pop();
	
	@Ensures ({"size()== old(size())+1", "peek()==old(obj)"})
	public void push(T obj);
	
 
}
